Inference at * 1 2 2 
Iof proof for Lemma sub-equality:

.....set predicate..... NILNIL

1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
7. P(i)
  {j:T| P(j)}  

latex

 by Assert u  {j:T| P(j)}  

latex

 1: .....assertion..... NILNIL

 1:   u  {j:T| P(j)} 
 2: 

 2: 8. u  {j:T| P(j)} 
 2:   {j:T| P(j)} 
 .

Definitions

t  T, {x:A| B(x)} , f(a)